LiDAR-based SLAM is a core technology for autonomous vehicles and robots. Despite the intense research activity in this field, each proposed system uses a particular sensor post-processing pipeline and a single map representation format. The present work aims at introducing a revolutionary point of view for 3D LiDAR SLAM and localization: (1) using view-based maps as the fundamental representation of maps ("simple-maps"), which can then be used to generate arbitrary metric maps optimized for particular tasks; and (2) by introducing a new framework in which mapping pipelines can be defined without coding, defining the connections of a network of reusable blocks much like deep-learning networks are designed by connecting layers of standardized elements. Moreover, the idea of including the current linear and angular velocity vectors as variables to be optimized within the ICP loop is also introduced, leading to superior robustness against aggressive motion profiles without an IMU. The presented open-source ecosystem, released to ROS 2, includes tools and prebuilt pipelines covering all the way from data acquisition to map editing and visualization, real-time localization, loop-closure detection, or map georeferencing from consumer-grade GNSS receivers. Extensive experimental validation reveals that the proposal compares well to, or improves, former state-of-the-art (SOTA) LiDAR odometry systems, while also successfully mapping some hard sequences where others diverge. A proposed self-adaptive configuration has been used, without parameter changes, for all 3D LiDAR datasets with sensors between 16 and 128 rings, extensively tested on 83 sequences over more than 250~km of automotive, hand-held, airborne, and quadruped LiDAR datasets, both indoors and outdoors. The open-sourced implementation is available online at https://github.com/MOLAorg/mola

Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel step-optimal plans. A bottleneck in this approach is to *prove the absence* of plans of a certain length. Specifically, if the optimal plan has N steps, then it is typically very costly to prove that there is no plan of length N-1. We pursue the idea of leading this proof within solution length preserving abstractions (over-approximations) of the original planning task. This is promising because the abstraction may have a much smaller state space; related methods are highly successful in model checking. In particular, we design a novel abstraction technique based on which one can, in several widely used planning benchmarks, construct abstractions that have exponentially smaller state spaces while preserving the length of an optimal plan. Surprisingly, the idea turns out to appear quite hopeless in the context of planning as satisfiability. Evaluating our idea empirically, we run experiments on almost all benchmarks of the international planning competitions up to IPC 2004, and find that even hand-made abstractions do not tend to improve the performance of SATPLAN. Exploring these findings from a theoretical point of view, we identify an interesting phenomenon that may cause this behavior. We compare various planning-graph based CNF encodings F of the original planning task with the CNF encodings F_abs of the abstracted planning task. We prove that, in many cases, the shortest resolution refutation for F_abs can never be shorter than that for F. This suggests a fundamental weakness of the approach, and motivates further investigation of the interplay between declarative transition-systems, over-approximating abstractions, and SAT encodings.